The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(2^n, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

minus(n__0, Y) → 0
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0, n__s(Y)) → 0
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0 → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X

Rewrite Strategy: FULL

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(2ⁿ):
The rewrite sequence
activate(n__s(n__div(n__s(X29820_3), n__s(Y30785_3)))) →⁺ s(if(geq(activate(X29820_3), activate(Y30785_3)), n__s(n__div(n__minus(activate(X29820_3), activate(Y30785_3)), n__s(activate(Y30785_3)))), n__0))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0,0,0].
The pumping substitution is [X29820_3 / n__s(n__div(n__s(X29820_3), n__s(Y30785_3)))].
The result substitution is [ ].

The rewrite sequence
activate(n__s(n__div(n__s(X29820_3), n__s(Y30785_3)))) →⁺ s(if(geq(activate(X29820_3), activate(Y30785_3)), n__s(n__div(n__minus(activate(X29820_3), activate(Y30785_3)), n__s(activate(Y30785_3)))), n__0))
gives rise to a decreasing loop by considering the right hand sides subterm at position [0,1,0,0,0].
The pumping substitution is [X29820_3 / n__s(n__div(n__s(X29820_3), n__s(Y30785_3)))].
The result substitution is [ ].

(2) BOUNDS(2^n, INF)

(3) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

minus(n__0, Y) → 0'
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0', n__s(Y)) → 0'
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0' → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0'
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X

S is empty.
Rewrite Strategy: FULL

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

TRS:
Rules:
minus(n__0, Y) → 0'
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0', n__s(Y)) → 0'
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0' → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0'
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X

Types:
minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__0 :: n__0:n__s:n__minus:n__div
0' :: n__0:n__s:n__minus:n__div
n__s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
activate :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
geq :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → true:false
true :: true:false
false :: true:false
div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
if :: true:false → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
hole_n__0:n__s:n__minus:n__div1_3 :: n__0:n__s:n__minus:n__div
hole_true:false2_3 :: true:false
gen_n__0:n__s:n__minus:n__div3_3 :: Nat → n__0:n__s:n__minus:n__div

(7) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
minus, activate, geq

They will be analysed ascendingly in the following order:
minus = activate
minus = geq
activate = geq

(8) Obligation:

TRS:
Rules:
minus(n__0, Y) → 0'
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0', n__s(Y)) → 0'
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0' → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0'
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X

Types:
minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__0 :: n__0:n__s:n__minus:n__div
0' :: n__0:n__s:n__minus:n__div
n__s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
activate :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
geq :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → true:false
true :: true:false
false :: true:false
div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
if :: true:false → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
hole_n__0:n__s:n__minus:n__div1_3 :: n__0:n__s:n__minus:n__div
hole_true:false2_3 :: true:false
gen_n__0:n__s:n__minus:n__div3_3 :: Nat → n__0:n__s:n__minus:n__div

Generator Equations:
gen_n__0:n__s:n__minus:n__div3_3(0) ⇔ n__0
gen_n__0:n__s:n__minus:n__div3_3(+(x, 1)) ⇔ n__s(gen_n__0:n__s:n__minus:n__div3_3(x))

The following defined symbols remain to be analysed:
activate, minus, geq

They will be analysed ascendingly in the following order:
minus = activate
minus = geq
activate = geq

(9) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
activate(gen_n__0:n__s:n__minus:n__div3_3(n5_3)) → gen_n__0:n__s:n__minus:n__div3_3(n5_3), rt ∈ Ω(1 + n5₃)

Induction Base:
activate(gen_n__0:n__s:n__minus:n__div3_3(0)) →_R^Ω(1)
gen_n__0:n__s:n__minus:n__div3_3(0)

Induction Step:
activate(gen_n__0:n__s:n__minus:n__div3_3(+(n5_3, 1))) →_R^Ω(1)
s(activate(gen_n__0:n__s:n__minus:n__div3_3(n5_3))) →_IH
s(gen_n__0:n__s:n__minus:n__div3_3(c6_3)) →_R^Ω(1)
n__s(gen_n__0:n__s:n__minus:n__div3_3(n5_3))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(10) Complex Obligation (BEST)

(11) Obligation:

TRS:
Rules:
minus(n__0, Y) → 0'
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0', n__s(Y)) → 0'
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0' → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0'
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X

Types:
minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__0 :: n__0:n__s:n__minus:n__div
0' :: n__0:n__s:n__minus:n__div
n__s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
activate :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
geq :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → true:false
true :: true:false
false :: true:false
div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
if :: true:false → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
hole_n__0:n__s:n__minus:n__div1_3 :: n__0:n__s:n__minus:n__div
hole_true:false2_3 :: true:false
gen_n__0:n__s:n__minus:n__div3_3 :: Nat → n__0:n__s:n__minus:n__div

Lemmas:
activate(gen_n__0:n__s:n__minus:n__div3_3(n5_3)) → gen_n__0:n__s:n__minus:n__div3_3(n5_3), rt ∈ Ω(1 + n5₃)

Generator Equations:
gen_n__0:n__s:n__minus:n__div3_3(0) ⇔ n__0
gen_n__0:n__s:n__minus:n__div3_3(+(x, 1)) ⇔ n__s(gen_n__0:n__s:n__minus:n__div3_3(x))

The following defined symbols remain to be analysed:
minus, geq

They will be analysed ascendingly in the following order:
minus = activate
minus = geq
activate = geq

(12) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
minus(gen_n__0:n__s:n__minus:n__div3_3(n845_3), gen_n__0:n__s:n__minus:n__div3_3(n845_3)) → gen_n__0:n__s:n__minus:n__div3_3(0), rt ∈ Ω(1 + n845₃ + n845₃²)

Induction Base:
minus(gen_n__0:n__s:n__minus:n__div3_3(0), gen_n__0:n__s:n__minus:n__div3_3(0)) →_R^Ω(1)
0' →_R^Ω(1)
n__0

Induction Step:
minus(gen_n__0:n__s:n__minus:n__div3_3(+(n845_3, 1)), gen_n__0:n__s:n__minus:n__div3_3(+(n845_3, 1))) →_R^Ω(1)
minus(activate(gen_n__0:n__s:n__minus:n__div3_3(n845_3)), activate(gen_n__0:n__s:n__minus:n__div3_3(n845_3))) →_L^{Ω(1 + n845₃)}
minus(gen_n__0:n__s:n__minus:n__div3_3(n845_3), activate(gen_n__0:n__s:n__minus:n__div3_3(n845_3))) →_L^{Ω(1 + n845₃)}
minus(gen_n__0:n__s:n__minus:n__div3_3(n845_3), gen_n__0:n__s:n__minus:n__div3_3(n845_3)) →_IH
gen_n__0:n__s:n__minus:n__div3_3(0)

We have rt ∈ Ω(n²) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n²).

(13) Complex Obligation (BEST)

(14) Obligation:

TRS:
Rules:
minus(n__0, Y) → 0'
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0', n__s(Y)) → 0'
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0' → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0'
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X

Types:
minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__0 :: n__0:n__s:n__minus:n__div
0' :: n__0:n__s:n__minus:n__div
n__s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
activate :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
geq :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → true:false
true :: true:false
false :: true:false
div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
if :: true:false → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
hole_n__0:n__s:n__minus:n__div1_3 :: n__0:n__s:n__minus:n__div
hole_true:false2_3 :: true:false
gen_n__0:n__s:n__minus:n__div3_3 :: Nat → n__0:n__s:n__minus:n__div

Lemmas:
activate(gen_n__0:n__s:n__minus:n__div3_3(n5_3)) → gen_n__0:n__s:n__minus:n__div3_3(n5_3), rt ∈ Ω(1 + n5₃)
minus(gen_n__0:n__s:n__minus:n__div3_3(n845_3), gen_n__0:n__s:n__minus:n__div3_3(n845_3)) → gen_n__0:n__s:n__minus:n__div3_3(0), rt ∈ Ω(1 + n845₃ + n845₃²)

Generator Equations:
gen_n__0:n__s:n__minus:n__div3_3(0) ⇔ n__0
gen_n__0:n__s:n__minus:n__div3_3(+(x, 1)) ⇔ n__s(gen_n__0:n__s:n__minus:n__div3_3(x))

The following defined symbols remain to be analysed:
geq, activate

They will be analysed ascendingly in the following order:
minus = activate
minus = geq
activate = geq

(15) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
geq(gen_n__0:n__s:n__minus:n__div3_3(n1969_3), gen_n__0:n__s:n__minus:n__div3_3(n1969_3)) → true, rt ∈ Ω(1 + n1969₃ + n1969₃²)

Induction Base:
geq(gen_n__0:n__s:n__minus:n__div3_3(0), gen_n__0:n__s:n__minus:n__div3_3(0)) →_R^Ω(1)
true

Induction Step:
geq(gen_n__0:n__s:n__minus:n__div3_3(+(n1969_3, 1)), gen_n__0:n__s:n__minus:n__div3_3(+(n1969_3, 1))) →_R^Ω(1)
geq(activate(gen_n__0:n__s:n__minus:n__div3_3(n1969_3)), activate(gen_n__0:n__s:n__minus:n__div3_3(n1969_3))) →_L^{Ω(1 + n1969₃)}
geq(gen_n__0:n__s:n__minus:n__div3_3(n1969_3), activate(gen_n__0:n__s:n__minus:n__div3_3(n1969_3))) →_L^{Ω(1 + n1969₃)}
geq(gen_n__0:n__s:n__minus:n__div3_3(n1969_3), gen_n__0:n__s:n__minus:n__div3_3(n1969_3)) →_IH
true

We have rt ∈ Ω(n²) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n²).

(16) Complex Obligation (BEST)

(17) Obligation:

TRS:
Rules:
minus(n__0, Y) → 0'
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0', n__s(Y)) → 0'
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0' → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0'
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X

Types:
minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__0 :: n__0:n__s:n__minus:n__div
0' :: n__0:n__s:n__minus:n__div
n__s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
activate :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
geq :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → true:false
true :: true:false
false :: true:false
div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
if :: true:false → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
hole_n__0:n__s:n__minus:n__div1_3 :: n__0:n__s:n__minus:n__div
hole_true:false2_3 :: true:false
gen_n__0:n__s:n__minus:n__div3_3 :: Nat → n__0:n__s:n__minus:n__div

Lemmas:
activate(gen_n__0:n__s:n__minus:n__div3_3(n5_3)) → gen_n__0:n__s:n__minus:n__div3_3(n5_3), rt ∈ Ω(1 + n5₃)
minus(gen_n__0:n__s:n__minus:n__div3_3(n845_3), gen_n__0:n__s:n__minus:n__div3_3(n845_3)) → gen_n__0:n__s:n__minus:n__div3_3(0), rt ∈ Ω(1 + n845₃ + n845₃²)
geq(gen_n__0:n__s:n__minus:n__div3_3(n1969_3), gen_n__0:n__s:n__minus:n__div3_3(n1969_3)) → true, rt ∈ Ω(1 + n1969₃ + n1969₃²)

Generator Equations:
gen_n__0:n__s:n__minus:n__div3_3(0) ⇔ n__0
gen_n__0:n__s:n__minus:n__div3_3(+(x, 1)) ⇔ n__s(gen_n__0:n__s:n__minus:n__div3_3(x))

The following defined symbols remain to be analysed:
activate, minus

They will be analysed ascendingly in the following order:
minus = activate
minus = geq
activate = geq

(18) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
activate(gen_n__0:n__s:n__minus:n__div3_3(n2634_3)) → gen_n__0:n__s:n__minus:n__div3_3(n2634_3), rt ∈ Ω(1 + n2634₃)

Induction Base:
activate(gen_n__0:n__s:n__minus:n__div3_3(0)) →_R^Ω(1)
gen_n__0:n__s:n__minus:n__div3_3(0)

Induction Step:
activate(gen_n__0:n__s:n__minus:n__div3_3(+(n2634_3, 1))) →_R^Ω(1)
s(activate(gen_n__0:n__s:n__minus:n__div3_3(n2634_3))) →_IH
s(gen_n__0:n__s:n__minus:n__div3_3(c2635_3)) →_R^Ω(1)
n__s(gen_n__0:n__s:n__minus:n__div3_3(n2634_3))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(19) Complex Obligation (BEST)

(20) Obligation:

TRS:
Rules:
minus(n__0, Y) → 0'
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0', n__s(Y)) → 0'
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0' → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0'
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X

Types:
minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__0 :: n__0:n__s:n__minus:n__div
0' :: n__0:n__s:n__minus:n__div
n__s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
activate :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
geq :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → true:false
true :: true:false
false :: true:false
div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
if :: true:false → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
hole_n__0:n__s:n__minus:n__div1_3 :: n__0:n__s:n__minus:n__div
hole_true:false2_3 :: true:false
gen_n__0:n__s:n__minus:n__div3_3 :: Nat → n__0:n__s:n__minus:n__div

Lemmas:
activate(gen_n__0:n__s:n__minus:n__div3_3(n2634_3)) → gen_n__0:n__s:n__minus:n__div3_3(n2634_3), rt ∈ Ω(1 + n2634₃)
minus(gen_n__0:n__s:n__minus:n__div3_3(n845_3), gen_n__0:n__s:n__minus:n__div3_3(n845_3)) → gen_n__0:n__s:n__minus:n__div3_3(0), rt ∈ Ω(1 + n845₃ + n845₃²)
geq(gen_n__0:n__s:n__minus:n__div3_3(n1969_3), gen_n__0:n__s:n__minus:n__div3_3(n1969_3)) → true, rt ∈ Ω(1 + n1969₃ + n1969₃²)

Generator Equations:
gen_n__0:n__s:n__minus:n__div3_3(0) ⇔ n__0
gen_n__0:n__s:n__minus:n__div3_3(+(x, 1)) ⇔ n__s(gen_n__0:n__s:n__minus:n__div3_3(x))

The following defined symbols remain to be analysed:
minus

They will be analysed ascendingly in the following order:
minus = activate
minus = geq
activate = geq

(21) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
minus(gen_n__0:n__s:n__minus:n__div3_3(n3500_3), gen_n__0:n__s:n__minus:n__div3_3(n3500_3)) → gen_n__0:n__s:n__minus:n__div3_3(0), rt ∈ Ω(1 + n3500₃ + n3500₃²)

Induction Base:
minus(gen_n__0:n__s:n__minus:n__div3_3(0), gen_n__0:n__s:n__minus:n__div3_3(0)) →_R^Ω(1)
0' →_R^Ω(1)
n__0

Induction Step:
minus(gen_n__0:n__s:n__minus:n__div3_3(+(n3500_3, 1)), gen_n__0:n__s:n__minus:n__div3_3(+(n3500_3, 1))) →_R^Ω(1)
minus(activate(gen_n__0:n__s:n__minus:n__div3_3(n3500_3)), activate(gen_n__0:n__s:n__minus:n__div3_3(n3500_3))) →_L^{Ω(1 + n3500₃)}
minus(gen_n__0:n__s:n__minus:n__div3_3(n3500_3), activate(gen_n__0:n__s:n__minus:n__div3_3(n3500_3))) →_L^{Ω(1 + n3500₃)}
minus(gen_n__0:n__s:n__minus:n__div3_3(n3500_3), gen_n__0:n__s:n__minus:n__div3_3(n3500_3)) →_IH
gen_n__0:n__s:n__minus:n__div3_3(0)

We have rt ∈ Ω(n²) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n²).

(22) Complex Obligation (BEST)

(23) Obligation:

TRS:
Rules:
minus(n__0, Y) → 0'
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0', n__s(Y)) → 0'
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0' → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0'
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X

Types:
minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__0 :: n__0:n__s:n__minus:n__div
0' :: n__0:n__s:n__minus:n__div
n__s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
activate :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
geq :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → true:false
true :: true:false
false :: true:false
div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
if :: true:false → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
hole_n__0:n__s:n__minus:n__div1_3 :: n__0:n__s:n__minus:n__div
hole_true:false2_3 :: true:false
gen_n__0:n__s:n__minus:n__div3_3 :: Nat → n__0:n__s:n__minus:n__div

Lemmas:
activate(gen_n__0:n__s:n__minus:n__div3_3(n2634_3)) → gen_n__0:n__s:n__minus:n__div3_3(n2634_3), rt ∈ Ω(1 + n2634₃)
minus(gen_n__0:n__s:n__minus:n__div3_3(n3500_3), gen_n__0:n__s:n__minus:n__div3_3(n3500_3)) → gen_n__0:n__s:n__minus:n__div3_3(0), rt ∈ Ω(1 + n3500₃ + n3500₃²)
geq(gen_n__0:n__s:n__minus:n__div3_3(n1969_3), gen_n__0:n__s:n__minus:n__div3_3(n1969_3)) → true, rt ∈ Ω(1 + n1969₃ + n1969₃²)

Generator Equations:
gen_n__0:n__s:n__minus:n__div3_3(0) ⇔ n__0
gen_n__0:n__s:n__minus:n__div3_3(+(x, 1)) ⇔ n__s(gen_n__0:n__s:n__minus:n__div3_3(x))

No more defined symbols left to analyse.

(24) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n²) was proven with the following lemma:
minus(gen_n__0:n__s:n__minus:n__div3_3(n3500_3), gen_n__0:n__s:n__minus:n__div3_3(n3500_3)) → gen_n__0:n__s:n__minus:n__div3_3(0), rt ∈ Ω(1 + n3500₃ + n3500₃²)

(25) BOUNDS(n^2, INF)

(26) Obligation:

TRS:
Rules:
minus(n__0, Y) → 0'
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0', n__s(Y)) → 0'
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0' → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0'
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X

Types:
minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__0 :: n__0:n__s:n__minus:n__div
0' :: n__0:n__s:n__minus:n__div
n__s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
activate :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
geq :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → true:false
true :: true:false
false :: true:false
div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
if :: true:false → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
hole_n__0:n__s:n__minus:n__div1_3 :: n__0:n__s:n__minus:n__div
hole_true:false2_3 :: true:false
gen_n__0:n__s:n__minus:n__div3_3 :: Nat → n__0:n__s:n__minus:n__div

Lemmas:
activate(gen_n__0:n__s:n__minus:n__div3_3(n2634_3)) → gen_n__0:n__s:n__minus:n__div3_3(n2634_3), rt ∈ Ω(1 + n2634₃)
minus(gen_n__0:n__s:n__minus:n__div3_3(n3500_3), gen_n__0:n__s:n__minus:n__div3_3(n3500_3)) → gen_n__0:n__s:n__minus:n__div3_3(0), rt ∈ Ω(1 + n3500₃ + n3500₃²)
geq(gen_n__0:n__s:n__minus:n__div3_3(n1969_3), gen_n__0:n__s:n__minus:n__div3_3(n1969_3)) → true, rt ∈ Ω(1 + n1969₃ + n1969₃²)

Generator Equations:
gen_n__0:n__s:n__minus:n__div3_3(0) ⇔ n__0
gen_n__0:n__s:n__minus:n__div3_3(+(x, 1)) ⇔ n__s(gen_n__0:n__s:n__minus:n__div3_3(x))

No more defined symbols left to analyse.

(27) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n²) was proven with the following lemma:
minus(gen_n__0:n__s:n__minus:n__div3_3(n3500_3), gen_n__0:n__s:n__minus:n__div3_3(n3500_3)) → gen_n__0:n__s:n__minus:n__div3_3(0), rt ∈ Ω(1 + n3500₃ + n3500₃²)

(28) BOUNDS(n^2, INF)

(29) Obligation:

TRS:
Rules:
minus(n__0, Y) → 0'
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0', n__s(Y)) → 0'
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0' → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0'
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X

Types:
minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__0 :: n__0:n__s:n__minus:n__div
0' :: n__0:n__s:n__minus:n__div
n__s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
activate :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
geq :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → true:false
true :: true:false
false :: true:false
div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
if :: true:false → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
hole_n__0:n__s:n__minus:n__div1_3 :: n__0:n__s:n__minus:n__div
hole_true:false2_3 :: true:false
gen_n__0:n__s:n__minus:n__div3_3 :: Nat → n__0:n__s:n__minus:n__div

Lemmas:
activate(gen_n__0:n__s:n__minus:n__div3_3(n2634_3)) → gen_n__0:n__s:n__minus:n__div3_3(n2634_3), rt ∈ Ω(1 + n2634₃)
minus(gen_n__0:n__s:n__minus:n__div3_3(n845_3), gen_n__0:n__s:n__minus:n__div3_3(n845_3)) → gen_n__0:n__s:n__minus:n__div3_3(0), rt ∈ Ω(1 + n845₃ + n845₃²)
geq(gen_n__0:n__s:n__minus:n__div3_3(n1969_3), gen_n__0:n__s:n__minus:n__div3_3(n1969_3)) → true, rt ∈ Ω(1 + n1969₃ + n1969₃²)

Generator Equations:
gen_n__0:n__s:n__minus:n__div3_3(0) ⇔ n__0
gen_n__0:n__s:n__minus:n__div3_3(+(x, 1)) ⇔ n__s(gen_n__0:n__s:n__minus:n__div3_3(x))

No more defined symbols left to analyse.

(30) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n²) was proven with the following lemma:
minus(gen_n__0:n__s:n__minus:n__div3_3(n845_3), gen_n__0:n__s:n__minus:n__div3_3(n845_3)) → gen_n__0:n__s:n__minus:n__div3_3(0), rt ∈ Ω(1 + n845₃ + n845₃²)

(31) BOUNDS(n^2, INF)

(32) Obligation:

TRS:
Rules:
minus(n__0, Y) → 0'
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0', n__s(Y)) → 0'
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0' → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0'
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X

Types:
minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__0 :: n__0:n__s:n__minus:n__div
0' :: n__0:n__s:n__minus:n__div
n__s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
activate :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
geq :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → true:false
true :: true:false
false :: true:false
div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
if :: true:false → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
hole_n__0:n__s:n__minus:n__div1_3 :: n__0:n__s:n__minus:n__div
hole_true:false2_3 :: true:false
gen_n__0:n__s:n__minus:n__div3_3 :: Nat → n__0:n__s:n__minus:n__div

Lemmas:
activate(gen_n__0:n__s:n__minus:n__div3_3(n5_3)) → gen_n__0:n__s:n__minus:n__div3_3(n5_3), rt ∈ Ω(1 + n5₃)
minus(gen_n__0:n__s:n__minus:n__div3_3(n845_3), gen_n__0:n__s:n__minus:n__div3_3(n845_3)) → gen_n__0:n__s:n__minus:n__div3_3(0), rt ∈ Ω(1 + n845₃ + n845₃²)
geq(gen_n__0:n__s:n__minus:n__div3_3(n1969_3), gen_n__0:n__s:n__minus:n__div3_3(n1969_3)) → true, rt ∈ Ω(1 + n1969₃ + n1969₃²)

Generator Equations:
gen_n__0:n__s:n__minus:n__div3_3(0) ⇔ n__0
gen_n__0:n__s:n__minus:n__div3_3(+(x, 1)) ⇔ n__s(gen_n__0:n__s:n__minus:n__div3_3(x))

No more defined symbols left to analyse.

(33) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n²) was proven with the following lemma:
minus(gen_n__0:n__s:n__minus:n__div3_3(n845_3), gen_n__0:n__s:n__minus:n__div3_3(n845_3)) → gen_n__0:n__s:n__minus:n__div3_3(0), rt ∈ Ω(1 + n845₃ + n845₃²)

(34) BOUNDS(n^2, INF)

(35) Obligation:

TRS:
Rules:
minus(n__0, Y) → 0'
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0', n__s(Y)) → 0'
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0' → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0'
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X

Types:
minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__0 :: n__0:n__s:n__minus:n__div
0' :: n__0:n__s:n__minus:n__div
n__s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
activate :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
geq :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → true:false
true :: true:false
false :: true:false
div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
if :: true:false → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
hole_n__0:n__s:n__minus:n__div1_3 :: n__0:n__s:n__minus:n__div
hole_true:false2_3 :: true:false
gen_n__0:n__s:n__minus:n__div3_3 :: Nat → n__0:n__s:n__minus:n__div

Lemmas:
activate(gen_n__0:n__s:n__minus:n__div3_3(n5_3)) → gen_n__0:n__s:n__minus:n__div3_3(n5_3), rt ∈ Ω(1 + n5₃)
minus(gen_n__0:n__s:n__minus:n__div3_3(n845_3), gen_n__0:n__s:n__minus:n__div3_3(n845_3)) → gen_n__0:n__s:n__minus:n__div3_3(0), rt ∈ Ω(1 + n845₃ + n845₃²)

Generator Equations:
gen_n__0:n__s:n__minus:n__div3_3(0) ⇔ n__0
gen_n__0:n__s:n__minus:n__div3_3(+(x, 1)) ⇔ n__s(gen_n__0:n__s:n__minus:n__div3_3(x))

No more defined symbols left to analyse.

(36) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n²) was proven with the following lemma:
minus(gen_n__0:n__s:n__minus:n__div3_3(n845_3), gen_n__0:n__s:n__minus:n__div3_3(n845_3)) → gen_n__0:n__s:n__minus:n__div3_3(0), rt ∈ Ω(1 + n845₃ + n845₃²)

(37) BOUNDS(n^2, INF)

(38) Obligation:

TRS:
Rules:
minus(n__0, Y) → 0'
minus(n__s(X), n__s(Y)) → minus(activate(X), activate(Y))
geq(X, n__0) → true
geq(n__0, n__s(Y)) → false
geq(n__s(X), n__s(Y)) → geq(activate(X), activate(Y))
div(0', n__s(Y)) → 0'
div(s(X), n__s(Y)) → if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
if(true, X, Y) → activate(X)
if(false, X, Y) → activate(Y)
0' → n__0
s(X) → n__s(X)
div(X1, X2) → n__div(X1, X2)
minus(X1, X2) → n__minus(X1, X2)
activate(n__0) → 0'
activate(n__s(X)) → s(activate(X))
activate(n__div(X1, X2)) → div(activate(X1), X2)
activate(n__minus(X1, X2)) → minus(X1, X2)
activate(X) → X

Types:
minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__0 :: n__0:n__s:n__minus:n__div
0' :: n__0:n__s:n__minus:n__div
n__s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
activate :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
geq :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → true:false
true :: true:false
false :: true:false
div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
s :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
if :: true:false → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__div :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
n__minus :: n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div → n__0:n__s:n__minus:n__div
hole_n__0:n__s:n__minus:n__div1_3 :: n__0:n__s:n__minus:n__div
hole_true:false2_3 :: true:false
gen_n__0:n__s:n__minus:n__div3_3 :: Nat → n__0:n__s:n__minus:n__div

Lemmas:
activate(gen_n__0:n__s:n__minus:n__div3_3(n5_3)) → gen_n__0:n__s:n__minus:n__div3_3(n5_3), rt ∈ Ω(1 + n5₃)

Generator Equations:
gen_n__0:n__s:n__minus:n__div3_3(0) ⇔ n__0
gen_n__0:n__s:n__minus:n__div3_3(+(x, 1)) ⇔ n__s(gen_n__0:n__s:n__minus:n__div3_3(x))

No more defined symbols left to analyse.

(39) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
activate(gen_n__0:n__s:n__minus:n__div3_3(n5_3)) → gen_n__0:n__s:n__minus:n__div3_3(n5_3), rt ∈ Ω(1 + n5₃)

(40) BOUNDS(n^1, INF)